Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:	app(id,x)	→ x
2:	app(add,0)	→ id
3:	app(app(add,app(s,x)),y)	→ app(s,app(app(add,x),y))
4:	app(app(map,f),nil)	→ nil
5:	app(app(map,f),app(app(cons,x),xs))	→ app(app(cons,app(f,x)),app(app(map,f),xs))

There are 7 dependency pairs:


6:	APP(app(add,app(s,x)),y)	→ APP(s,app(app(add,x),y))
7:	APP(app(add,app(s,x)),y)	→ APP(app(add,x),y)
8:	APP(app(add,app(s,x)),y)	→ APP(add,x)
9:	APP(app(map,f),app(app(cons,x),xs))	→ APP(app(cons,app(f,x)),app(app(map,f),xs))
10:	APP(app(map,f),app(app(cons,x),xs))	→ APP(cons,app(f,x))
11:	APP(app(map,f),app(app(cons,x),xs))	→ APP(f,x)
12:	APP(app(map,f),app(app(cons,x),xs))	→ APP(app(map,f),xs)

The approximated dependency graph contains one SCC: {7,9,11,12}.

Tyrolean Termination Tool (0.06 seconds) --- May 3, 2006